es{-}rcv{-}atom(${\it es}$;$e$;$a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\uparrow$es{-}isrcv(${\it es}$; $e$)) $\Rightarrow$ free{-}from{-}atom\{1\}(es{-}valtype(${\it es}$; $e$);es{-}val(${\it es}$; $e$);$a$)